| Definitions | IdLnk, Id,  x:A. B(x), x:A  B(x), Dsys, x:A B(x), P & Q, Feasible(D), False, P   Q,  A, {x:A| B(x) },  ,  b, Unit, left+right, M.state, locl(a), M.da(a), M sends on link l, queue(l;t), <a,b>, A B,  , nil, d-world(D;v;sched;dec), snds(l;t), source(l), M(i), M.dout2(l;tg),  x.A(x), Msg(M), type List, s = t, Type, t  T, i j, #$n, -n, n+m, n-m, a<b, Void, upto(n), {i..j },  x:A. B(x), Top, Msg, m(l;t), car.cdr, as @ bs, map(f;as), concat(ll), Prop,  b,  , i=j, P  Q, S  T, i j < k, onlnk(l;mss), m(i;t), 2of(t), State(ds), Knd, f(a), d-world-state(D;i), mlnk(m), a = b, filter(P;l),  x:A. B(x), P  Q, stutter-state(s), Msg(da), M.Msg, next-world-state(D;i;s;k;v), M.V(k), M.dout(l,tg), M.din(l,tg), d-decl(D;i), Valtype(da;k), M.sends(k,s,v), a = b, True,  T, P Q, msg(l;t;v), w.M, rcvs(l;t), destination(l), Action(i), ||as||, nth_tl(n;as) |
| Lemmas | nth tl wf, nth tl nil, non neg length, length wf1, w-action wf, ldst wf, w-rcvs wf, msg wf, ma-dout wf, assert-eq-lnk, assert-eq-id, squash wf, true wf, filter filter reduce, eq id wf, ma-send-val wf, d-decl-subtype, ma-send-val-nil2, ma-msg wf, mlnk wf d, subtype rel self, d-comp-step, filter wf, eq lnk wf, mlnk wf, append nil sq, concat-cons, append wf, concat wf, concat append, map wf, w-ml wf, w-Msg wf, d-world wf, top wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, map append sq, int seg wf, upto wf, le wf, ge wf, not wf, assert wf, ma-sends-on wf, d-feasible wf, ma-da wf, locl wf, ma-st wf, nat wf, unit wf, dsys wf, nat properties, Msg wf, ma-dout2 wf, d-m wf, lsrc wf, Id wf, IdLnk wf |
dec:(i,a:Id